Example 16 in [ Lucas - IC'06]

Summary: Ex16_Luc06

• TPDB format
• OBJ format
• Negative results:
  1. Lucas' transformation
• Positive results:
  1. CSDP
  2. Ferreira and Ribeiro's transformation
  3. Giesl and Middeldorp's transformation
  4. Zantema's transformation

Ex16_Luc06 in TPDB format ( Ex16_Luc06.trs):

(VAR X)
(STRATEGY CONTEXTSENSITIVE 
  (f 1)
  (a)
  (b)
)
(RULES 
f(X,X) -> f(a,b)
b -> a
)

The CS-TRS in OBJ format (file Ex15_Luc06.obj):

obj Ex16_Luc06 is
  sort S .
  op f : S S -> S [strat (1 0)] .
  op a : -> S .
  op b : -> S .
  vars X : S .
  eq f(X,X) = f(a,b) .
  eq b = a .
endo

Negative results

1. The µ-termination of Ex16_Luc06 cannot be proved by using Lucas' transformation. The TRS Ex16_Luc06_L:

   f(X) -> f(a)
   b -> a
   
   	
   

   is not terminating (AProVE).
   

Positive results

1. The µ-termination of Ex16_Luc06 can be proved by using CSDP (computed by MuTerm ).
2. The µ-termination of Ex16_Luc06 can be proved by using Ferreira and Ribeiro's or Zantema's transformation. The transformed TRS Ex16_Luc06:

   					 
   	f(X,X) -> f(a,n__b)
   	b -> a
   	b -> n__b
   	activate(n__b) -> b
   	activate(X) -> X
   	
   	

   can be proved terminating by AProVE
3. The µ-termination of Ex16_Luc06 can be proved by using Giesl and Middeldorp's transformation. The TRS Ex16_Luc06_GM:

   					
   	a__f(X,X) -> a__f(a,b)
   	a__b -> a
   	mark(f(X1,X2)) -> a__f(mark(X1),X2)
   	mark(b) -> a__b
   	mark(a) -> a
   	a__f(X1,X2) -> f(X1,X2)
   	a__b -> b
   		
   	

   can be proved terminating by AProVE